Java Modeling Language
part 7/8 · 12.1 KB total
──────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────
• Sireum/Kiasan, a symbolic execution based static analyzer which supports JML as a contract language.
• JMLUnit, a tool to generate files for running JUnit tests on JML annotated Java files.
• TACO, an open source program analysis tool that statically checks the compliance of a Java program against its Java Modeling Language specification.
References
• Gary T. Leavens and Yoonsik Cheon. Design by Contract with JML; Draft tutorial.
• Gary T. Leavens, Albert L. Baker, and Clyde Ruby. JML: A Notation for Detailed Design; in Haim Kilov, Bernhard Rumpe, and Ian Simmonds (editors), Behavioral Specifications of Businesses and Systems, Kluwer, 1999, chapter 12, pages 175-188.
• Gary T. Leavens, Erik Poll, Curtis Clifton, Yoonsik Cheon, Clyde Ruby, David Cok, Peter Müller, Joseph Kiniry, Patrice Chalin, and Daniel M. Zimmerman. JML Reference Manual (DRAFT), September 2009. HTML
• Marieke Huisman, Wolfgang Ahrendt, Daniel Bruns, and Martin Hentschel. Formal specification with JML. 2014. download (CC-BY-NC-ND)
──────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────